依值类型论

依值类型论（Dependent type theory）是一种强大而富有表达力的语言，允许你表达复杂的数学断言，编写复杂的硬件和软件规范，并以自然和统一的方式对这两者进行推理。Lean是基于一个被称为构造演算（Calculus of Constructions）的依值类型论的版本，它拥有一个可数的非累积性宇宙（non-cumulative universe）的层次结构以及归纳类型（inductive type）。在本章结束时，你将学会一大部分。

“类型论”得名于其中每个表达式都有一个类型。举例：在一个给定的语境中，x + 0可能表示一个自然数，f可能表示一个定义在自然数上的函数。Lean中的自然数是任意精度的无符号整数。

这里的一些例子展示了如何声明对象以及检查其类型。

位于/-和-/之间的文本组成了一个注释块，会被Lean的编译器忽略。类似地，两条横线--后面也是注释。注释块可以嵌套，这样就可以“注释掉”一整块代码，这和任何程序语言都是一样的。

def关键字声明工作环境中的新常量符号。在上面的例子中，def m : Nat := 1定义了一个Nat类型的新常量m，其值为1。#check命令要求Lean给出它的类型，用于向系统询问信息的辅助命令都以井号(#)开头。#eval命令让Lean计算给出的表达式。你应该试试自己声明一些常量和检查一些表达式的类型。

普通类型论的强大之处在于，你可以从其他类型中构建新的类型。例如，如果a和b是类型，a -> b表示从a到b的函数类型，a × b表示由a元素与b元素配对构成的类型，也称为笛卡尔积。注意×是一个Unicode符号，可以使用\times或简写\tim来输入。合理使用Unicode提高了易读性，所有现代编辑器都支持它。在Lean标准库中，你经常看到希腊字母表示类型，Unicode符号→是->的更紧凑版本。

同样，你应该自己尝试一些例子。

让我们看一些基本语法。你可以通过输入\to或者\r或者\->来输入→。你也可以就用ASCII码->，所以表达式Nat -> Nat和Nat → Nat意思是一样的，都表示以一个自然数作为输入并返回一个自然数作为输出的函数类型。Unicode符号×是笛卡尔积，用\times输入。小写的希腊字母α，β，和γ等等常用来表示类型变量，可以用\a，\b，和\g来输入。

这里还有一些需要注意的事情。第一，函数f应用到值x上写为f x(例：Nat.succ 2)。第二，当写类型表达式时，箭头是右结合的；例如，Nat.add的类型是Nat → Nat → Nat，等价于Nat → (Nat → Nat)。

因此你可以把Nat.add看作一个函数，它接受一个自然数并返回另一个函数，该函数接受一个自然数并返回一个自然数。在类型论中，把Nat.add函数看作接受一对自然数作为输入并返回一个自然数作为输出的函数通常会更方便。系统允许你“部分应用”函数Nat.add，比如Nat.add 3具有类型Nat → Nat，即Nat.add 3返回一个“等待”第二个参数n的函数，然后可以继续写Nat.add 3 n。

注：取一个类型为Nat × Nat → Nat的函数，然后“重定义”它，让它变成Nat → Nat → Nat类型，这个过程被称作柯里化（currying）。

如果你有m : Nat和n : Nat，那么(m, n)表示m和n组成的有序对，其类型为Nat × Nat。这个方法可以制造自然数对。反过来，如果你有p : Nat × Nat，之后你可以写p.1 : Nat和p.2 : Nat。这个方法用于提取它的两个组件。

Lean所依据的依值类型论对普通类型论的其中一项升级是，类型本身（如Nat和Bool这些东西）也是对象，因此也具有类型。

上面的每个表达式都是类型为Type的对象。你也可以为类型声明新的常量:

正如上面所示，你已经看到了一个类型为Type → Type → Type的函数例子，即笛卡尔积 Prod：

这里有另一个例子：给出任意类型α，那么类型List α是类型为α的元素的列表的类型。

看起来Lean中任何表达式都有一个类型，因此你可能会想到：Type自己的类型是什么？

实际上，这是Lean系统的一个最微妙的方面：Lean的底层基础有无限的类型层次：

可以将Type 0看作是一个由“小”或“普通”类型组成的宇宙。然后，Type 1是一个更大的类型范围，其中包含Type 0作为一个元素，而Type 2是一个更大的类型范围，其中包含Type 1作为一个元素。这个列表是不确定的，所以对于每个自然数n都有一个Type n。Type是Type 0的缩写：

然而，有些操作需要在类型宇宙上具有多态（polymorphic）。例如，List α应该对任何类型的α都有意义，无论α存在于哪种类型的宇宙中。所以函数List有如下的类型：

这里u_1是一个覆盖类型级别的变量。#check命令的输出意味着当α有类型Type n时，List α也有类型Type n。函数Prod具有类似的多态性：

你可以使用 universe 命令来声明宇宙变量，这样就可以定义多态常量：

可以通过在定义F时提供universe参数来避免使用universe命令：

Lean提供 fun (或 λ)关键字用于从给定表达式创建函数，如下所示：

你可以通过传递所需的参数来计算lambda函数：

从另一个表达式创建函数的过程称为lambda 抽象。假设你有一个变量x : α和一个表达式t : β，那么表达式fun (x : α) => t或者λ (x : α) => t是一个类型为α → β的对象。这个从α到β的函数把任意x映射到t。

这有些例子：

Lean将这三个例子解释为相同的表达式；在最后一个表达式中，Lean可以从表达式if not y then x + 1 else x + 2推断x和y的类型。

一些数学上常见的函数运算的例子可以用lambda抽象的项来描述:

看看这些表达式的意思。表达式fun x : Nat => x代表Nat上的恒等函数，表达式fun x : Nat => true表示一个永远输出true的常值函数，表达式fun x : Nat => g (f x)表示f和g的复合。一般来说，你可以省略类型注释，让Lean自己推断它。因此你可以写fun x => g (f x)来代替fun x : Nat => g (f x)。

你可以以函数作为参数，通过给它们命名f和g，你可以在实现中使用这些函数：

你还可以以类型作为参数：

这个表达式表示一个接受三个类型α，β和γ和两个函数g : β → γ和f : α → β，并返回的g和f的复合的函数。(理解这个函数的类型需要理解依值乘积类型，下面将对此进行解释。)

lambda表达式的一般形式是fun x : α => t，其中变量x是一个“约束变量”：它实际上是一个占位符，其“作用域”没有扩展到表达式t之外。例如，表达式fun (b : β) (x : α) => b中的变量b与前面声明的常量b没有任何关系。事实上，这个表达式表示的函数与fun (u : β) (z : α) => u是一样的。形式上，可以通过给约束变量重命名来使形式相同的表达式被看作是alpha等价的，也就是被认为是“一样的”。Lean认识这种等价性。

注意到项t : α → β应用到项s : α上导出了表达式t s : β。回到前面的例子，为清晰起见给约束变量重命名，注意以下表达式的类型:

表达式(fun x : Nat => x) 1的类型是Nat。实际上，应用(fun x : Nat => x)到1上返回的值是1。

稍后你将看到这些项是如何计算的。现在，请注意这是依值类型论的一个重要特征：每个项都有一个计算行为，并支持“标准化”的概念。从原则上讲，两个可以化约为相同形式的项被称为“定义等价”。它们被Lean的类型检查器认为是“相同的”，并且Lean尽其所能地识别和支持这些识别结果。

Lean是个完备的编程语言。它有一个生成二进制可执行文件的编译器，和一个交互式解释器。你可以用#eval命令执行表达式，这也是测试你的函数的好办法。

注意到#eval和#reduce不是等价的。#eval命令首先把Lean表达式编译成中间表示（intermediate representation, IR）然后用一个解释器来执行这个IR。某些内建类型（例如，Nat、String、Array）在IR中有更有效率的表示。IR支持使用对Lean不透明的外部函数。 #reduce命令建立在一个化简引擎上，类似于在Lean的可信内核中使用的那个，它是负责检查和验证表达式和证明正确性的那一部分。它的效率不如#eval，且将所有外部函数视为不透明的常量。之后你将了解到这两个命令之间还有其他一些差异。

def关键字提供了一个声明新对象的重要方式。

这很类似其他编程语言中的函数。名字double被定义为一个函数，它接受一个类型为Nat的输入参数x，其结果是x + x，因此它返回类型Nat。然后你可以调用这个函数:

在这种情况下你可以把def想成一种lambda。下面给出了相同的结果：

当Lean有足够的信息来推断时，你可以省略类型声明。类型推断是Lean的重要组成部分:

定义的一般形式是def foo : α := bar，其中α是表达式bar返回的类型。Lean通常可以推断类型α，但是精确写出它可以澄清你的意图，并且如果定义的右侧没有匹配你的类型，Lean将标记一个错误。

bar可以是任何一个表达式，不只是一个lambda表达式。因此def也可以用于给一些值命名，例如：

def可以接受多个输入参数。比如定义两自然数之和：

参数列表可以像这样分开写：

注意到这里我们使用了double函数来创建add函数的第一个参数。

你还可以在def中写一些更有趣的表达式：

你可能能猜到这个可以做什么。

还可以定义一个函数，该函数接受另一个函数作为输入。下面调用一个给定函数两次，将第一次调用的输出传递给第二次:

现在为了更抽象一点，你也可以指定类型参数等：

这句代码的意思是：函数compose首先接受任何两个函数作为参数，这其中两个函数各自接受一个输入。类型β → γ和α → β意思是要求第二个函数的输出类型必须与第一个函数的输入类型匹配，否则这两个函数将无法复合。

compose再接受一个类型为α的参数作为第二个函数（这里叫做f）的输入，通过这个函数之后的返回结果类型为β，再作为第一个函数（这里叫做g）的输入。第一个函数返回类型为γ，这就是compose函数最终返回的类型。

compose可以在任意的类型α β γ上使用，它可以复合任意两个函数，只要前一个的输出类型是后一个的输入类型。举例：

Lean还允许你使用let关键字来引入“局部定义”。表达式let a := t1; t2定义等价于把t2中所有的a替换成t1的结果。

这里twice_double x定义等价于(x + x) * (x + x)。

你可以连续使用多个let命令来进行多次替换：

换行可以省略分号;。

表达式let a := t1; t2的意思很类似(fun a => t2) t1，但是这两者并不一样。前者中你要把t2中每一个a的实例考虑成t1的一个缩写。后者中a是一个变量，表达式fun a => t2不依赖于a的取值而可以单独具有意义。作为一个对照，考虑为什么下面的foo定义是合法的，但bar不行（因为在确定了x所属的a是什么之前，是无法让它+ 2的）。

考虑下面这三个函数定义：

Lean提供variable指令来让这些声明变得紧凑：

你可以声明任意类型的变量，不只是Type类型：

输出结果表明所有三组定义具有完全相同的效果。

variable命令指示Lean将声明的变量作为约束变量插入定义中，这些定义通过名称引用它们。Lean足够聪明，它能找出定义中显式或隐式使用哪些变量。因此在写定义时，你可以将α、β、γ、g、f、h和x视为固定的对象，并让Lean自动抽象这些定义。

当以这种方式声明时，变量将一直保持存在，直到所处理的文件结束。然而，有时需要限制变量的作用范围。Lean提供了小节标记section来实现这个目的：

当一个小节结束后，变量不再发挥作用。

你不需要缩进一个小节中的行。你也不需要命名一个小节，也就是说，你可以使用一个匿名的section /end对。但是，如果你确实命名了一个小节，你必须使用相同的名字关闭它。小节也可以嵌套，这允许你逐步增加声明新变量。

Lean可以让你把定义放进一个“命名空间”（namespace）里，并且命名空间也是层次化的：

当你声明你在命名空间Foo中工作时，你声明的每个标识符都有一个前缀Foo.。在打开的命名空间中，可以通过较短的名称引用标识符，但是关闭命名空间后，必须使用较长的名称。与section不同，命名空间需要一个名称。只有一个匿名命名空间在根级别上。

open命令使你可以在当前使用较短的名称。通常，当你导入一个模块时，你会想打开它包含的一个或多个命名空间，以访问短标识符。但是，有时你希望将这些信息保留在一个完全限定的名称中，例如，当它们与你想要使用的另一个命名空间中的标识符冲突时。因此，命名空间为你提供了一种在工作环境中管理名称的方法。

例如，Lean把和列表相关的定义和定理都放在了命名空间List之中。

open List命令允许你使用短一点的名字：

像小节一样，命名空间也是可以嵌套的：

关闭的命名空间可以之后重新打开，甚至是在另一个文件里：

与小节一样，嵌套的名称空间必须按照打开的顺序关闭。命名空间和小节有不同的用途：命名空间组织数据，小节声明变量，以便在定义中插入。小节对于分隔set_option和open等命令的范围也很有用。

然而，在许多方面，namespace ... end结构块和section ... end表现出来的特征是一样的。尤其是你在命名空间中使用variable命令时，它的作用范围被限制在命名空间里。类似地，如果你在命名空间中使用open命令，它的效果在命名空间关闭后消失。

简单地说，类型可以依赖于参数。你已经看到了一个很好的例子：类型List α依赖于参数α，而这种依赖性是区分List Nat和List Bool的关键。另一个例子，考虑类型Vector α n，即长度为n的α元素的向量类型。这个类型取决于两个参数：向量中元素的类型α : Type和向量的长度n : Nat。

假设你希望编写一个函数cons，它在列表的开头插入一个新元素。cons应该有什么类型？这样的函数是多态的（polymorphic）：你期望Nat，Bool或任意类型α的cons函数表现相同的方式。因此，将类型作为cons的第一个参数是有意义的，因此对于任何类型α，cons α是类型α列表的插入函数。换句话说，对于每个α，cons α是将元素a : α插入列表as : List α的函数，并返回一个新的列表，因此有cons α a as : List α。

很明显，cons α具有类型α → List α → List α，但是cons具有什么类型？如果我们假设是Type → α → list α → list α，那么问题在于，这个类型表达式没有意义：α没有任何的所指，但它实际上指的是某个类型Type。换句话说，假设α : Type是函数的首个参数，之后的两个参数的类型是α和List α，它们依赖于首个参数α。

这就是依值函数类型，或者依值箭头类型的一个例子。给定α : Type和β : α → Type，把β考虑成α之上的类型族，也就是说，对于每个a : α都有类型β a。在这种情况下，类型(a : α) → β a表示的是具有如下性质的函数f的类型：对于每个a : α，f a是β a的一个元素。换句话说，f返回值的类型取决于其输入。

注意到(a : α) → β对于任意表达式β : Type都有意义。当β的值依赖于a（例如，在前一段的表达式β a），(a : α) → β表示一个依值函数类型。当β的值不依赖于a，(a : α) → β与类型α → β无异。实际上，在依值类型论（以及Lean）中，α → β表达的意思就是当β的值不依赖于a时的(a : α) → β。【注】

译者注：在依值类型论的数学符号体系中，依值类型是用Π符号来表达的，在Lean 3中还使用这种表达，例如Π x : α, β x。Lean 4抛弃了这种对新手不友好的写法，但是沿袭了三代中另外两种意义更明朗的写法：forall x : α, β x和∀ x : α, β x。这几个表达式都和(x : α) → β x同义。但是个人感觉本教程这一段的讲法也对新手不友好，(x : α) → β x这种写法在引入“构造子”之后意义会更明朗一些（见下一个注释），当前反倒是forall x : α, β x这种写法对于来自数学背景的读者更加清楚明白，关于前一种符号在量词与等价一章中有更详细的说明。同时，依值类型有着更丰富的引入动机，推荐读者寻找一些拓展读物。

回到列表的例子，你可以使用#check命令来检查下列的List函数。@符号以及圆括号和花括号之间的区别将在后面解释。

就像依值函数类型(a : α) → β a通过允许β依赖α从而推广了函数类型α → β，依值笛卡尔积类型(a : α) × β a同样推广了笛卡尔积α × β。依值积类型又称为sigma类型，可写成Σ a : α, β a。你可以用⟨a, b⟩或者Sigma.mk a b来创建依值对。

函数f和g表达的是同样的函数。

假设我们有一个列表的实现如下：

然后，你可以建立一个自然数列表如下：

由于构造子对类型是多态的【注】，我们需要重复插入类型Nat作为一个参数。但是这个信息是多余的：我们可以推断表达式Lst.cons Nat 5 (Lst.nil Nat)中参数α的类型，这是通过第二个参数5的类型是Nat来实现的。类似地，我们可以推断Lst.nil Nat中参数的类型，这是通过它作为函数Lst.cons的一个参数，且这个函数在这个位置需要接收的是一个具有Lst α类型的参数来实现的。

译者注：“构造子”（constructor）的概念前文未加解释，对类型论不熟悉的读者可能会困惑。它指的是一种“依值类型的类型”，也可以看作“类型的构造器”，例如λ α : α -> α甚至可看成⋆ -> ⋆。当给α或者⋆赋予一个具体的类型时，这个表达式就成为了一个类型。前文中(x : α) → β x中的β就可以看成一个构造子，(x : α)就是传进的类型参数。原句“构造子对类型是多态的”意为给构造子中放入不同类型时它会变成不同类型。

这是依值类型论的一个主要特征：项包含大量信息，而且通常可以从上下文推断出一些信息。在Lean中，我们使用下划线_来指定系统应该自动填写信息。这就是所谓的“隐参数”。

然而，敲这么多下划线仍然很无聊。当一个函数接受一个通常可以从上下文推断出来的参数时，Lean允许你指定该参数在默认情况下应该保持隐式。这是通过将参数放入花括号来实现的，如下所示:

唯一改变的是变量声明中α : Type u周围的花括号。我们也可以在函数定义中使用这个技巧：

这使得ident的第一个参数是隐式的。从符号上讲，这隐藏了类型的说明，使它看起来好像ident只是接受任何类型的参数。事实上，函数id在标准库中就是以这种方式定义的。我们在这里选择一个非传统的名字只是为了避免名字的冲突。

variable命令也可以用这种技巧来来把变量变成隐式的：

Lean有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些“洞”或“占位符”的过程通常被称为繁饰（elaboration）。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像id或List.nil这样的表达式被认为是“多态的”，因为它可以在不同的上下文中具有不同的含义。

可以通过写(e : T)来指定表达式e的类型T。这就指导Lean的繁饰器在试图解决隐式参数时使用值T作为e的类型。在下面的第二个例子中，这种机制用于指定表达式id和List.nil所需的类型:

Lean中数字是重载的，但是当数字的类型不能被推断时，Lean默认假设它是一个自然数。因此，下面的前两个#check命令中的表达式以同样的方式进行了繁饰，而第三个#check命令将2解释为整数。

然而，有时我们可能会发现自己处于这样一种情况：我们已经声明了函数的参数是隐式的，但现在想显式地提供参数。如果foo是有隐参数的函数，符号@foo表示所有参数都是显式的该函数。

第一个#check命令给出了标识符的类型id，没有插入任何占位符。而且，输出表明第一个参数是隐式的。